A:MsgA. ma-frame-compatible(A;) 

latex

Definitions	t  T, , x:A. B(x), P  Q, MsgA, ma-frame-compatible(A;B)
Lemmas	msga wf, ma-frame-compatible symmetry, ma-empty-frame-compatible-left, ma-empty wf